i:Id, k:Knd. has-src(i;k)  isrcv(k) & source(lnk(k)) = i 

latex

Definitions	1of(t), x. t(x), IdLnk, False, True, P  Q, P & Q, P  Q, has-src(i;k), A & B, Prop, b, isrcv(k), source(l), lnk(k), x:A. B(x), P  Q, Knd, t  T, Id
Lemmas	Id wf, Knd wf, lnk wf, lsrc wf, isrcv wf, assert wf, has-src wf, IdLnk wf, pi1 wf, assert-eq-id